@i events of kind k change x to f State(ds) (val:T)
== (x:Id. vartype(i;x)  ds(x)?Top) & kindtype(i;k)  T
== & e@i. kind(e) = k  valtype(e)  T & (x after e) = f((state when e),val(e)) 

latex

---

clarification:

effect-p(es;i;ds;k;T;x;f)
== (x:Id. es-vartype(es; i; x)  fpf-cap(ds;IdDeq;x;Top)) & es-kindtype(es;i;k)  T
== & alle-at(es;i;e.es-kind(es; e) = k  Knd
== & alle-at(es;i;e. es-valtype(es; e)  T
== & alle-at(es;i;e. & es-after(es; x; e)
== & alle-at(es;i;e. & =
== & alle-at(es;i;e. & f(es-state-when(es;e),es-val(es; e))
== & alle-at(es;i;e. &  fpf-cap(ds;IdDeq;x;Top)) 

latex

Definitions	P & Q, x:A. B(x), Id, vartype(i;x), kindtype(i;k), e@i. P(e), P  Q, Knd, kind(e), A & B, valtype(e), s = t, f(x)?z, IdDeq, Top, (x after e), f(a), (state when e), val(e)
FDL editor aliases	effect-p